Here are the essentials:
Here1. For any two terms a and b, we intend 'a ~ b' to be a type (in U{1})
Here2. For any term a, 'a ~ a'
Here3. For two terms a and b, 'a ~ b' if b computes to a (normal
Here3. direct computation)
Here4. For any of the following types T, and two terms a, b in T, we
Here4. For have 'a = b in T => a ~ b'
Here4. a. int
Here4. b. Atom
Here4. c. any equality type (such as Unit)
Here5. Two terms 'opid1{params1}(a1, ..., an)' and 'opid2{params2}(b1, ..., bn)'
Here5. are squiggle equal if opid1 and opid2 are the same,
Here5. params1 and params2 are the same, the arity of the terms is
Here5. the same, and 'a1 ~ b1', ..., 'an ~ bn'
Here5. -- This rule is not strictly necessary, given the substitution
Here5. rule, and the reflexive rule, but it is pretty useful in any case.
Here6. Substitution: if 'T[a]' is a hypothesis or conclusion in a
Here6. sequent, and 'a ~ b', then 'T[a]' can be replaced by 'T[b]'
Here6. (and there is no need to prove functionality).
We don't have a rule for proving when two squiggle types are equal, so
we can't use the squiggle type as a hypothesis. If we had one, the
rule would be something like this:
rule'a ~ b = c ~ d in U1'
if 'a ~ b <=> c ~ d' and all free variables in a, b, c, and d belong to
"canonical" types (T is a canonical type if
'all a, b: T. a = b in T => a ~ b').